% FIXED!
\section{AAD Definitions}
\label{s:prelim:notation:dictionaries}

\parhead{Notation.}
% Note: Recall that a (total) function maps every element in its domain. Its range are all the values that are mapped to some domain key. Its codomain are all the possible values in the universe, including unmapped ones. In contrast, partial function does not map every element in the domain.
Let $|S|$ denote the number of elements in a multiset $S$ (e.g., $S=\{1,2,2\}$ and $|S|=3$).
Let $\mathcal{K}$ be the set of all possible keys and $\mathcal{V}$ be the set of all possible values.
($\mathcal{K}$ and $\mathcal{V}$ are application-specific; e.g., in software transparency, a key is the software package name and a value is the hash of a specific version of this software package.)
Formally, a \textit{dictionary} is a function $D : K \rightarrow \mathcal{P}(\mathcal{V})$ that maps a key $k\in K$ to a multiset of values $V\in\mathcal{P}(\mathcal{V})$ (including the empty set), where $K\subset \mathcal{K}$ and $\mathcal{P}(\mathcal{V})$ denotes all possible multisets with elements from $\mathcal{V}$.
Thus, $D(k)$ denotes the multiset of values associated with key $k$ in dictionary $D$.
Let $|D|$ denote the number of key-value pairs in the dictionary or its \textit{version}.
Appending $(k,v)$ to a version $i$ dictionary updates the multiset $V = D(k)$ of key $k$ to $V' = V \cup \{v\}$ and increments the dictionary version to $i+1$.

\parhead{Server-side API.}
The untrusted server implements:
\vspace{.5em}

\api {\setup}$(1^\lambda, \beta) \rightarrow pp, VK$.
Randomized algorithm that returns public parameters $pp$ used by the server and a \textit{verification key} $VK$ used by clients.
Here, $\lambda$ is a security parameter and $\beta$ is an upper-bound on the number of elements $n$ in the dictionary (i.e., $n \le \beta$).

\api {\append}$(pp, \AD_i, d_i, k,v) \rightarrow \AD_{i+1}, d_{i+1}$.
Deterministic algorithm that appends a new key-value pair $(k,v)$ to the version $i$ dictionary, creating a new version $i+1$ dictionary.
Succeeds only if the dictionary is not full (i.e., $i + 1 \le \beta$).
Returns the new authenticated dictionary $\AD_{i+1}$ and its digest $d_{i+1}$.

\api $\provelookup(pp, \AD_i, k) \rightarrow V, \pi_{k,V}$.
Deterministic algorithm that generates a proof $\pi_{k,V}$ that $V$ is the \textit{complete} multiset of values for key $k$.
In particular, when $\AD_i(k) = \varnothing$, this is a proof that key $k$ has no values.
Finally, the server cannot construct a fake proof $\pi_{k,V'}$ for the wrong $V'$, including for $V' = \varnothing$.

\api {\proveappendonly}$(pp, \AD_i, \AD_j) \rightarrow \pi_{i, j}$.
Deterministic algorithm that proves $\AD_i$ is a subset of $\AD_j$.
Generates an \textit{append-only proof} $\pi_{i, j}$ that all key-value pairs in $\AD_i$ are also present and unchanged in $\AD_j$.
Importantly, a malicious server who removed or changed keys from $\AD_j$ that were present in $\AD_i$ cannot construct a valid append-only proof.

\parhead{Client-side API.}
Clients implement:
\vspace{.5em}

\api {\verlookup}$(VK, d_i, k, V, \pi) \rightarrow \{T, F\}$.
Deterministic algorithm that verifies proofs returned by $\provelookup(\cdot)$ against the digest $d_i$ at version $i$ of the dictionary.
When $V \ne \varnothing$, verifies that $V$ is the complete multiset of values for key $k$, ensuring no values have been left out and no extra values were added.
When $V = \varnothing$, verifies that key $k$ is not mapped to any value.

\api {\verappendonly}$(VK, d_i, i, d_j, j, \pi_{i,j}) \rightarrow \{T, F\}$.
Deterministic algorithm that ensures a dictionary remains append-only.
Verifies that $\pi_{i,j}$ correctly proves that the dictionary with digest $d_i$ is a subset of the dictionary with digest $d_j$.
Also, verifies that $d_i$ and $d_j$ are digests of dictionaries at version $i$ and $j$, respectively.

\parhead{AAD Correctness and Security Definitions.}
Consider an ordered sequence of $n$ key-value pairs $(k_i\in \mathcal{K}, v_i\in\mathcal{V})_{i\in [n]}$.
Note that the same key (or key-value pair) can occur multiple times in the sequence.
% --- begin multiline ---
Let 
$\AD',d' \leftarrow \multiappend(pp, \AD, d, (k_i, v_i)_{i\in [n]})$ 
denote a sequence of $\append(\cdot)$ calls arbitrarily interleaved with other $\provelookup(\cdot)$ and $\proveappendonly(\cdot)$ calls such that 
% NOTE: Can force \newline in inline equations but is there a better way?
$\AD',d'$ $\leftarrow$ $\append(pp,\AD_{n-1}, d_{n-1}, k_{n}, v_n)$,
$\AD_{n-1}, d_{n-1}$ $\leftarrow$ $\append(pp,\AD_{n-2}$, $d_{n-2}, k_{n-1}, v_{n-1})$,
$\dots$,
$\AD_{1}, d_1$ $\leftarrow$ $\append(pp,\AD, d, k_{1}, v_{1})$.
% --- end of multiline ---
Let $D_n$ denote the \textit{corresponding dictionary} obtained after appending each $(k_i, v_i)_{i\in [n]}$ in order.
%In other words, $\kv{k,v}\in D_n \Leftrightarrow \exists i\in [n]$ s.t. $k=k_i$ and $v=v_i$.
Finally, let $\AD_0$ denote an empty authenticated dictionary with (empty) digest $d_0$.

\begin{definition}[Append-only Authenticated Dictionary]
    \label{d:secure-maad-definition}
    (\setup, \append, \provelookup, \proveappendonly, \verlookup, \verappendonly) is a secure append-only authenticated dictionary (AAD) if
    $\exists$ negligible function $\negl$,
    $\forall$ security parameters $\lambda$,  $\forall$ upper-bounds $\beta=\poly(\lambda)$ and $\forall n \le \beta$ it satisfies the following properties:
\end{definition}

\parhead{Lookup correctness.}
\label{s:aad:lookup-correctness}
$\forall$ sequences $(k_i\in \mathcal{K}, v_i\in\mathcal{V})_{i\in [n]}$ with corresponding dictionary $D_n$, $\forall$ keys $k\in\mathcal{K}$,
\begin{align*}
\Pr \left[ \begin{array}{c}
    (pp,VK) \leftarrow \setup(1^\lambda, \beta),\\
    (\AD, d) \leftarrow \multiappend(pp, \AD_0, d_0, (k_i, v_i)_{i\in [n]}),\\
    (V, \pi) \leftarrow \provelookup(pp,\AD, k): \\
    {V = D_n(k)} \wedge {\verlookup(VK, d, k, V,\pi) = T}
\end{array} \right] \ge 1 - \negl(\lambda)
\end{align*}

\noindent \textit{Observation:}
Note that this definition compares the returned multiset $V$ with the ``ground truth'' in $D_n$ and thus provides lookup correctness.
Also, it handles non-membership correctness since $V$ can be the empty set.
Finally, the definition handles all possible orders of inserting key-value pairs.

\parhead{Lookup security.}
\label{s:aad:lookup-security}
$\forall$ adversaries \textsf{A} running in time $\mathsf{poly}(\lambda)$,
%\end{definition}
\begin{align*}
\small
\Pr \left[ \begin{array}{c}
    (pp,VK) \leftarrow \setup(1^\lambda, \beta), \\
    (d, k,V\ne V',\pi,\pi') \leftarrow \mathsf{A}(pp, VK)
    : \\
    {\verlookup(VK,d, k,V,\pi) = T} \wedge {} \\
    {\verlookup(VK,d, k,V',\pi') = T}
\end{array} \right] \le \negl(\lambda)
\end{align*}

\noindent \textit{Observation:}
This definition captures the lack of any ``ground truth'' about what was inserted in the dictionary, since there is no trusted source in our model.
Nonetheless, given a fixed digest $d$, our definition prevents \textit{all} equivocation attacks about the complete multiset of values of a key, including the special case where the server equivocates about the key being present (i.e., $V \ne \varnothing$ and $V' = \varnothing$).
% Note that this definition also implies that different dictionaries cannot have the same digest.
% Suppose I have two different dictionaries with the same digest.
% Then, there must a key k with different multisets V and V'.
% Membership correctness says proofs for V and V' can be constructed w.r.t. to the digest.
% However, this breaks membership security.

\parhead{Append-only correctness.}
\label{s:aad:appendonly-correctness}
$\forall$ sequences $(k_i\in \mathcal{K}, v_i\in\mathcal{V})_{i\in [n]}$ where $n\ge 2$
\begin{align*}
\small
\Pr \left[ \begin{array}{c}
    (pp,VK) \leftarrow \setup(1^\lambda, \beta) \\
    (\AD_m, d_m) \leftarrow \multiappend(pp,\AD_0,d_0,(k_i, v_i)_{i\in [m]}),\\
    (\AD_n, d_n) \leftarrow \multiappend(pp,\AD_m,d_m,(k_j, v_j)_{j\in [m+1,n]}),  \\
    \pi \leftarrow \proveappendonly(pp,\AD_m, \AD_n):\\
    {\verappendonly(VK, d_m, m, d_n, n, \pi) = T}
\end{array} \right] \ge 1 - \negl(\lambda)
\end{align*}

% Note: This does not subsume lookup security when i = j because, according to this definition, V = [v1] and V' = [v1,v2] would both be allowed as the multisets for key k in the same digest d_i
\parhead{Append-only security.}
\label{s:aad:appendonly-security}
$\forall$ adversaries \textsf{A} running in time $\mathsf{poly}(\lambda)$,
\begin{align*}
\small
\Pr \left[ \begin{array}{c}
    (pp,VK) \leftarrow \setup(1^\lambda, \beta)\\
    (d_i,d_j,i<j,\pi_a, k,V, V',\pi,\pi') \leftarrow \mathsf{A}(pp, VK)
    : \\
    {\verappendonly(VK, d_i, i, d_j, j, \pi_a) = T} \wedge {}\\
    {\verlookup(VK, d_i, k, V , \pi )  = T} \wedge {}\\
    {\verlookup(VK, d_j, k, V', \pi') = T} \wedge {}\\
    {V\not\subset V' \wedge V\ne V'}
\end{array} \right] \le \negl(\lambda)
\end{align*}

% NOTE: In an earlier version, we forgot to restrict that V \not\subset V' in addition to V\ne V'.
% Without the subset restriction, V\ne V' would mean normal appends are counted as "append-only breaks": e.g., a valid append of a new value v_2 to a key k, would go from a set V = {v_1} of values to a larger set V' = {v_1, v_2} with V\ne V'.
%
% Instead, what we want is to guarantee that either the old set of values V be a subset of the new ones V', or that V = V'.
% In other words, if V \not\subset V' and V \ne V', then the append-only property was broken

\noindent \textit{Observation:}
This definition ensures that values can only be added to a key and can never be removed nor changed.

\parhead{Fork consistency.}
This definition stays the same as in \cref{s:aas:fork-consistency}.
